perm filename EQUIVA[W88,JMC] blob
sn#881539 filedate 1990-01-26 generic text, type C, neo UTF8
COMMENT ā VALID 00008 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 %equiva[w88,jmc] Equivalence classes as first class objects
C00008 00003 \section{The Proposal}
C00012 00004 \section{An Example}
C00017 00005 \section{Remarks}
C00018 00006 \section{References:}
C00019 00007 \smallskip\centerline{Copyright \copyright\ 1990\ by John McCarthy}
C00020 00008 leftovers
C00021 ENDMK
Cā;
%equiva[w88,jmc] Equivalence classes as first class objects
\input memo.tex[let,jmc]
\title{EQUIVALENCE CLASSES AS FIRST CLASS OBJECTS}
\section{The Problem}
In mathematics, two of the main operations for constructing
new sorts of entities from old are cartesian product and forming
the set of equivalence classes under an equivalence relation. Two
initial examples are prominent in mathematics. The rationals are
defined as equivalence classes of pairs of integers, and the
integers themselves are defined as equivalence classes of pairs
of natural numbers.
Many programming languages allow cartesian product as a
way of forming new data ``types'', e.g. as records. This makes
tuples of objects of previously defined ``types'' into first
class objects. However, defining a new ``type'' by forming the
set of equivalence classes under an equivalence relation isn't
provided for in any language I know of.
It isn't accidental that programming languages provide
for cartesian products and don't provide for sets of equivalence
classes. The goal of equivalence classes is mentioned in (McCarthy
1963) which first, I think, proposed cartesian product as a way
of forming new sorts of data. Providing cartesian products is
straightforward and providing sets of equivalence classes is
impossible unless the rules are changed.
Namely, it isn't hard to implement a standard
way of representing elements of cartesian products, i.e.
tuples of objects, by data
structures that provides reasonable efficiency---especially when
cartesian products are not used recursively. Therefore, the
implementer of the language can provide for them in a
straightforward manner. (Even so, cartesian products are often
not treated as first class objects, because the implementers
forget to provide a notation for constants in the new domain.)
Providing for equivalence classes is much harder. There
isn't any standard efficient way of of representing them. A natural
proposal for representing equivalence classes is to pick a
member of each equivalence class as the representative of the
class. This is often the right thing to do, but it may depend on
some mathematics. For example, when we regard the rationals as
equivalence classes of pairs of integers, we normally choose as
representative of a class, the member in which the denominator is
positive and the numerator and denominator are relatively prime,
i.e. the fraction is in lowest terms. We can't expect a compiler
to invent the notion of a fraction in lowest terms.
Even if we could pick representatives in a natural way,
it is often not optimal to use representatives. For example, the
integers are often defined as equivalence classes of pairs of
natural numbers under the equivalence relation
%
$$(m,n) equiv (m',n') ā” m+n' = m'+n.$$
%
If we use representatives, this suggests choosing the one in which
either $m=0$ or $n=0$. However, it is usually more convenient to
use sign-magnitude notation, taking advantage of the fact that only
one more bit is required to represent an integer than to represent
its absolute value.
\section{The Proposal}
The above difficulties suggest a different way of
thinking about computations with equivalence classes. We propose
that programming languages should allow equivalence classes as
first class objects.
The language would allow a declaration like
%
$$declare Y = X mod R,$$
%
where $X$ is an existing data sort and $R$ is an equivalence
relation defined on $X$.
However, we give up the idea of a standard representation
of elements of sets.
Instead the user must supply by separate declarations information
about how these things are to be done. Of course, the user may have
programs to help him, including AI programs. Thus we are separating
the description of the algorithm {\it per se} from the description of
the data representation and the basic operations on the data types.
The program can be written and verified without deciding on
how sets of equivalence classes are to be represented. However,
before the program can be compiled or interpreted, the representations
must be declared.
Certain additional information must be supplied. Here are
some examples.
1. There is a canonical mapping $\phi$ from $X$ to to $Y$
projecting an element of $X$ into its equivalence class.
2. There may be mappings from $Y$ to $X$ taking classes
into ``standard'' representatives. How these representatives should
be chosen may depend on the application.
3. It is common to define operations on the equivalence classes
in terms of operations on representatives. Thus the arithmetic operations
on integers and rational numbers are defined in terms of certain
operations on the sets of pairs. In order to be well-defined,
these functions must commute with the projections. If the programmer
prescribes these operations incorrectly, they will not be well-defined.
There are two attitudes we can take. The first is to say that
defining operations is done at the programmer's risk. The second is
to require him to prove that the operations are well-defined. An
example of requiring proof that something is well-defined is provided
by the Boyer-Moore interactive theorem prover. While they are
interested in proofs of program properties and other mathematical
theorems, the analogy with their work may be exploitable in dealing
with equivalence classes.
4. It is often necessary to be able to index over sets of
equivalence classes, and this requires maps from the natural
numbers to the classes.
\section{An Example}
We illustrate these concepts with a substantial example.
\noindent The 15-puzzle.
My interest in equivalence classes as objects was revived
in connection with a heuristic program for the well-known 15-puzzle.
We will not take the space either to define the 15-puzzle or to
describe the program. We only give a few relevant facts.
A position in the 15-puzzle consists of a 1-1 mapping
from a set $T$ of 15 numbered tiles into a set $S$ of 16 squares arranged
in a $4\times 4$ array. Such a mapping leaves one square empty. The
object of the puzzle is to arrange the tiles in increasing numerical order
using a sequence of moves of a tile into the adjacent empty square.
There are $16!$ positions. The heuristic program uses a predicate
$better(p1,p2)$ defining a better position and does an iterative
deepening search to find a better position. If the position keeps
getting better and better we eventually win. This search of the
space of positions is feasible for a LISP machine, but several
thousand positions are often examined before a sequence of moves
leading to an improved position is found. This is far more searching
than a human does in deciding on a move.
The search space can be made much smaller if we take into
account the fact that at any stage of the solution we are interested
in the positions of only a few of the tiles. Specifically, in any
position arising in the puzzle, there is
an initial sequence of tiles that have already been put in their
final positions. In getting the next tile to its final position we
need only consider the position of that tile, the position of the
empty square and sometimes the position of the last tile placed.
All other previously placed tiles are locked into place.
Thus we consider set of the equivalence classes under the relation taking
as equivalent two positions related by a permutation of the remaining
14 or 13 tiles. This set contains $16\times 15 \times 14 = 3500$
elements, and only a subset of these actually occur in the
search.
The above isn't quite true for the last two rows, but
a suitably modified heuristic still requires only three positions
to be kept track of in the search.
Therefore, the problem is conveniently programmed in a
language that allows declaring the appropriate sets of equivalence
classes. However, the equivalence relation to be used depends on
which tile we are trying to move to its final position. Therefore,
we need to be able to declare sets of equivalence classes in blocks
of the program, and the equivalence relation used should depend on
the values of variables when the block is entered. In this respect
the language should resemble Algol 60 which allows declarations
in blocks depending on the values of variables rather than resembling
Pascal which doesn't allow dynamic declarations.
\section{Remarks}
I put ``type'' in quotes, because the computer science usage
differs from that of mathematical logic because of some ancient
carelessness. Logic uses types for higher order objects, e.g.
functions and predicates and forms hierarchies of types. It uses
the term ``sort'' for what computer science calls a type. The
computer science terminology is defective, because it doesn't
make the distinction, which will be important in computer science
as well as in logic.
\section{References:}
\noindent {\bf McCarthy, John (1963)}: ``A Basis for a Mathematical Theory of Computation'',
in P. Braffort and D. Hirschberg (eds.), {\it Computer Programming and
Formal Systems}, North-Holland Publishing Co., Amsterdam, pp. 33-70.
\smallskip\centerline{Copyright \copyright\ 1990\ by John McCarthy}
\smallskip\noindent{\fiverm This draft of EQUIVA[W88,JMC]\ TEXed on \jmcdate\ at \theTime}
%File originated on 24-Jan-90
\vfill\eject\end
leftovers
We also often need to be able to index over the members of an
equivalence class. There isn't a standard way of doing that either.
Indexing over sets is also directly allowed in the language.